@InCollection{SantiagoJúniorTaha:2016:TiPeFo,
               author = "Santiago J{\'u}nior, Valdivino Alexandre de and Tahar, S.",
                title = "Time performance formal evaluation of complex systems",
            booktitle = "Formal Methods: Foundations and Applications",
            publisher = "Springer",
                 year = "2016",
               editor = "Corn{\'e}lio, M{\'a}rcio and Roscoe, Bill",
                pages = "162--177",
             keywords = "Astrophysics, Balloons, Continuous time systems, Markov processes, 
                         Model checking, Numerical methods Computational technique, 
                         Continuous time Markov chain, Formal verification methods, 
                         Numerical computations, Performance analysis, Probabilistic model 
                         checking, Scientific experiments, Traditional techniques.",
             abstract = "Formal verification methods, such as Model Checking, have been 
                         used for addressing performance/dependability analysis of systems. 
                         Such formal methods have several advantages over traditional 
                         techniques aiming at performance/dependability analysis such as 
                         the use of a single computational technique for evaluation of any 
                         measure and all complex numerical computation steps are hidden to 
                         the user. This paper reports on the use of Probabilistic Model 
                         Checking for time performance evaluation of complex systems. We 
                         propose an approach, TPerP, that allows a professional to clearly 
                         address time performance analysis based on Continuous-Time Markov 
                         Chain (CTMC). Our approach takes into consideration several types 
                         of delay analyzes. We applied it to a balloon-borne high energy 
                         astrophysics scientific experiment where we dealt with CTMCs that 
                         had around 30 million reachable states and 75 million transitions, 
                         and we concluded that the current definition used in the balloon 
                         system is inadequate in terms of performance.",
          affiliation = "{Instituto Nacional de Pesquisas Espaciais (INPE)} and {Concordia 
                         University}",
                  doi = "10.1007/978-3-319-29473-5_10",
                  url = "http://dx.doi.org/10.1007/978-3-319-29473-5_10",
                 isbn = "978-331929472-8",
             language = "en",
          seriestitle = "Lecture Notes in Computer Science",
           targetfile = "valdivino_time.pdf",
               volume = "9526",
        urlaccessdate = "28 abr. 2024"
}